Z3: SMT Solving in Practice
Z3 is a powerful SMT solver used in many verification tools to reason about logical formulas, constraints, and program properties. In this project, students will select a problem that can be formulated as a constraint system or verification task, and solve it using Z3 directly.
Students are encouraged to bring their own ideas. Two example directions:
- Solve constraint puzzles (e.g., Sudoku, scheduling, resource allocation) using Z3’s built-in theories.
- Write a small symbolic executor for a simple language and use Z3 to check assertions or verify program paths.
The project should focus on showcasing Z3’s capabilities through meaningful examples, with complexity adapted to individual progress.